\begin{tabbing}
$\forall$\=$i$, $a$:Id, $T$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$Prop),\+
\\[0ex]${\it init}$:\{$f$:$x$:Id fp$\rightarrow$ ${\it ds}$($x$)?Void$\mid$ $\forall$$x$:Id. $x$ $\in$ dom(${\it ds}$) $\Leftrightarrow$ $x$ $\in$ dom($f$) \}.
\-\\[0ex]Normal($T$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}$). Dec($\exists$$v$:$T$. $P$($s$,$v$)))
\\[0ex]$\Rightarrow$ R{-}Feasible(R{-}pre{-}init($i$;${\it ds}$;${\it init}$;$a$;$T$;$P$))
\end{tabbing}